COMMENT ⊗   VALID 00003 PAGES 
RECORD PAGE   DESCRIPTION
 00001 00001
 00002 00002	.EVERY HEADING (Preliminary User's Manual , ,{DATE})
 00006 00003	VI. PRIMITIVE PATTERN LANGUAGE.
 00012 ENDMK
⊗;
.EVERY HEADING (Preliminary User's Manual , ,{DATE})

V. SEARCHING AND PATTERN MATCHING.

.BEGIN DOUBLE SPACE

This section is a preliminary account of certain features of the current system
which are being extended and developed further.

The pattern matching facilities for interactive theorem proving
are the most difficult feature to describe well. The tools presented to the
user should be general enough to significantly aid in the search for a proof.
At the same time the pattern matching commands should be concise and somewhat
readable.
Clearly, pattern matching is present throughout the theorem prover; the
choice strategies, the rules of inference, and the editing strategies are all
examples of very sophisticated pattern matching. Thus pattern matching is
 very important part of the theorem proving process. 
Currently, a very simple pattern matching facility is available.

Pattern matching is invoked by the FIND operation. FIND[<id>,<pattern>] expects
<id> to be the name of a list of clauses, and <pattern> should be a Boolean
combination of primitive patterns. These primitive patterns are described in the
next section, but basically allow description of syntactic parts of clauses.

Since many of the applications of FIND are of the form FIND[CLAUSES,<pattern>],
the abbreviation, FINDC[<pattern>] has been added for this case.

Here's an example of FIND and FINDC. 

.END
.BEGIN VERBATIM
SET XX FINDC[OCR[0]];  	|OCR is a reserved word. The pattern says
			|find all clauses in the set CLAUSES which 
			|have occurrences of the symbol 0.
			|In this problem 0 is a function letter.
*
DI XX;			|Display the clauses.

1 x/y=0 ⊃ x≤y;
2 x≤y ⊃ x/y=0;
3 0≤x;
4 x/x=0;
5 x/1=0;
*

SET YY FIND[XX,OCR[≤]];	|Find all clauses in XX which have occurrences
			|of the symbol '≤', and assign those clauses 
			|to YY.
*
DI YY;			|Display YY.
1 x/y=0 ⊃ x≤y;
2 x≤y ⊃ x/y=0;
*

*
SET ZZ FIND[YY,OCR[/]∧OCR[=]];|Boolean combinations are allowed.
*
SET ZZ FIND[YY,LENGTH=1];|This command will locate all units in the 
			|set, YY.
.END
.NEXT PAGE
VI. PRIMITIVE PATTERN LANGUAGE.

.BEGIN DOUBLE SPACE

The currently available primitives allow description of  ancestry of a clause,
the length(number of literals) and depth(of function nesting) of clauses,besides
a very simple matching algorithm.  The matcher  looks for matches on literals
,terms, predicate letters, negations of predicate letters, or fuctions symbols.


PRIMITIVES:

1) primitive for ancestry:  TREE[x]

"x" designates a clause.  TREE[x] will match any clause whose derivation tree
contains x.  N.B.  the clause ,x, itself is considered to be derived from x.

Examples:

For example, if G1 is the name of an initial statement then :

SET YY FIND[XX,TREE[G1]]; will assign to YY all of the clauses in XX which
were derived using G1.

2) primitive for length:   LENGTH

LENGTH gives the number of literals in the clauses currenly being examined.
LENGTH may be tested using one of the available operators.

Examples:

LENGTH = 1 is true of the current clauses is a unit.

3) primitive for depth:    DEPTH

This primitive gives the depth of function nesting in the clause.

Example:

DEPTH > 4 is true is the depth of nesting of the current clause is greater
than 4.
.END

.BEGIN VERBATIM

Primitive relations:

Currently the only relations available are  =,>,and <.  These relations
are only to be used in comparing length and depth.

.END

.BEGIN DOUBLE SPACE

MATCHING:

4) primitive for matching: OCR

OCR is the implementation of a simple matcher which expects its arguments
to be a literal, term,  predicate letter, or negation of a predicate letter.
OCR matches any clause which contains a matching construct.

Variables may appear in the pattern, in which case  a test for subsumption
determines when a match is to be successful.

Examples:

In the following, assume P, and = are predicate letters; assume x,y, and
z are variables; and assume a,b,c,d and f and g are function symbols.

OCR[P] matches P(x) ,P(a)⊃a=b, and ¬P(b).

OCR[¬P] matches P(a)⊃a=b and ¬P(b). Note P(a)⊃a=b matches here since the
implication really is ¬P(a) ∨ a=b;

OCR[¬=]∧¬OCR[d] would match ¬f(a,b)=c but would not match ¬f(a,b)=d.

OCR[P(x)] matches P(x),¬P(g(x)) and ¬P(a).

OCR[¬P(g(x))] matches ¬P(g(a)) but not P(g(a)) or ¬P(f(g(a),x));

OCR[f(g(x),x)] matches clauses containing say, f(g(a),a) but does not match
f(g(a)b).
.END